RCS "$Id: MuCalculusFuns.sig,v 1.7 1998/08/13 11:38:54 pxs Exp $";
signature MU_CALCULUS_FUNS =
sig
   structure L   : MU_CALCULUS_PROTECTED

   val propenv  : ((L.param list * L.prop) E.env ref)
   val printPropEnv : unit -> unit
   val propDefString : V.var -> string	(* may raise E.Unbound *)
   val simplifyWithNegation : L.prop -> L.prop
(* return a prop in which as well as "simplify": *)
(* negations have been removed *)
(* variables have been renamed so as to be unique IN A SPECIAL ORDER for*)
(* model-checking! See GameCheck.str before altering the order! *)
(* Also return a list of the user-chosen variable names, in reverse order *)
(* of the names we give them (so the last var in the list is the one we call *)
(* 0, etc. This can be used to print props in a user-comprehensible way! *)
   val simplifyWithoutNegation : L.prop -> (L.prop * string list)
   val usesValues : L.prop -> bool     
end

